1. $T$ : Type
\\[0ex]2. $P$ : $T$$\rightarrow\mathbb{P}$
\\[0ex]3. $f$ : $\forall$$x$:$T$. Dec($P$($x$))
\\[0ex]4. $x$ : $T$
\\[0ex]$\vdash$  ($\uparrow$isl(case $f$($x$) of inl($p$) =$>$ inr $p$  $\mid$ inr($p$) =$>$ inl $x$ )) $\Leftarrow\!\Rightarrow$ ($\neg$$P$($x$))